perm filename CHOICE.NEW[1,JRA] blob
sn#005827 filedate 1972-09-28 generic text, type T, neo UTF8
00100 (DE REENTER()
00110 (COND(ANCESTRY(TRYPRF LLST))(T(TRYPRF CLAUSES))))
00120
00200
00300 (DEFPROP ATTEMPT
00400 (LAMBDA(L S C)
00500 (PROG (NEWNAME SUPPORT
00600 UNITPF
00700 LCL
00800 LVL
00900 CNT
01000 XYZ2
01100 LSTCLS
01200 LLST
01300 Z1
01400 MERGE
01500 ORDER
01600 DEBUG
01700 DEPTH
01800 LENGTH
01900 ANCESTRY
02000 STRATEGY
02100 STRAT
02200 PMODEL
02300 NMODEL
02400 PFLG
02500 EQUAL
02600 PDEPTH
02700 DLIST
02800 XYZ
02900 XYZ1
03000 COND
03100 Z
03200 UNAXP
03300 UNAXN
03400 SAT
03500 EXTERM
03600 E1
03700 E2
03800 B2
03900 XX
04000 CLAUSES
04100 SUBCLAUSES
04200 COUNT
04300 SLENGTH
04400 ORDLST
04500 OCLIST)
04600 (SETQ NEWNAME (LIST (LIST NIL)))
04700 (SETORD (CAR L) (CDR L))
04800 (SETQ Z (MINIMIZE (CAR L)))
04900 (UPDATESTATE (COND ((NULL S) (SETQ STRAT (SETQUERY Z))) (T (SETQ STRAT S))))
05000 (SETQ COND C)
05100 (SETQ XYZ2 Z)
05200 (SETQ LVL 1)
05300 (SETQ COUNT 0)
05400 (SETQ Z (UNITPN XYZ2))
05500 (SETQ UNAXP (CAR Z))
05600 (SETQ UNAXN (CDR Z))
05700 (SETQ CLAUSES XYZ2)
05800 (COND ((NOT PFLG) (SETQ UNAXP (CONS (SET2 (LIST (LIST 1 NIL) (LIST EQUAL 0 0))) UNAXP))
05900 (SETQ SUBCLAUSES (CONS (CAR UNAXP) CLAUSES)))
06000 (T (SETQ SUBCLAUSES CLAUSES)))
06100 (SETQ LCL (LAST CLAUSES))
06200 (SETQ LSTCLS LCL)
06300 (SETQ CNT (ADD1 (LENGTH XYZ2)))
06400 (SETQ AXNO 201)
06500 (SETQ Z1 (ERRSET (TRYPRF (COND (ANCESTRY (SETQ LLST (INITIAL XYZ2 -1000 1000))) (T XYZ2)))))
06600 (COND ((OR (EQ Z1 (QUOTE NOPROOF)) (NULL Z1)) (RETURN (CONS (QUOTE NOPROOF) (CONS CLAUSES STRAT))))
06700 ((EQ (CAR Z1) (QUOTE QED)) (SETQ Z
06800 (EVAL
06900 (LIST (QUOTE OUTC)
07000 (LIST (QUOTE OUTPUT) (QUOTE PRF) (QUOTE DSK:) FILENAM)
07100 NIL)))
07200 (QUERY)
07300 (PROOF LHP RHP)
07400 (OUTC Z T)
07500 (RETURN Z1))
07600 (T (RETURN Z1)))))
07700 EXPR)
07800
07900 (DEFPROP EDIT
08000 (LAMBDA(U Z)
08100 (PROG (RES1 U1 U4 )
08200 ED4 (COND ((NULL Z) (RETURN RES1)))
08300 (SETQ U4 (CAR Z))
08500 (COND ((OR (GREATERP (NUM U4) LENGTH) (GREATERP (DEPTH (CDR U4) ) DEPTH)) (GO ED2)))
08600 (SETQ U1 SUBCLAUSES)
08700 ED1 (COND ((SUBSUME (CAR U1) U4) (GO ED2)))
08800 ED6 (SETQ U1 (CDR U1))
08900 (COND (U1 (GO ED1)))
09000 (SETQ U1 (CDR Z))
09100 (COND ((NULL U1) (GO ED5)))
09200 ED3 (COND ((SUBSUME (CAR U1) U4) (GO ED2)))
09300 ED7 (SETQ U1 (CDR U1))
09400 (COND (U1 (GO ED3)))
09500 ED5 (SETQ RES1 (CONS U4 RES1))
09600 ED2 (SETQ Z (CDR Z))
09700 (GO ED4)))
09800 EXPR)
09900
10000 (DEFPROP SUBSUME
10100 (LAMBDA(C D)
10200 (COND ((OR (AND (ALLPOS C) (ALLNEG D)) (AND (ALLNEG C) (ALLPOS D))) NIL)
10300 ((OR (NOT (HERE C)) (NOT (HERE D))) NIL)
10400 ((NOT (GREATERP (NUM C) (NUM D))) (SUBSUME1 (CDR C) (POSBIT C) (CDR D) (POSBIT D) NIL))
10500 (T NIL)))
10600 EXPR)
10700
10800 (DEFPROP BOOKEEP
10900 (LAMBDA(L M N)
11000 (PROG (U U1)
11100 B1 (SETQ U M)
11200 (SETQ U1 U)
11300 B3 (RPLACD (CDAAR U) (CONS 0 N))
11400 (SETQ U (CDR U))
11500 (COND ((NULL U) (RPLACD L M) (RETURN U1)))
11600 (SETQ U1 (CDR U1))
11700 (GO B3)))
11800 EXPR)
11900
12000 (DEFPROP CHOICE
12100 (LAMBDA(X E1 B2 E2)
12200 (PROG (Z1 Z2)
12300 (SETQ Z1 (CAR X))
12400 (SETQ Z2 (CDR X))
12500 (COND ((NOT (EQ Z2 E2)) (RETURN (RPLACD X (CDR Z2))))
12600 ((EQ Z1 E1) (RETURN NIL))
12700 (T
12800 (RETURN
12900 (PROG2 (RPLACA X (CDR Z1)) (RPLACD X (COND (ANCESTRY (CHOICE1 (CADR Z1) B2)) (T B2)))))))))
13000 EXPR)
13100
13200 (DEFPROP FINI
13300 (LAMBDA(U R Z1 Z2 E)
13400 (PROG (Z)
13500 (COND (UFLG (SETQ R (UNITREDUCT R UNAXP UNAXN))))
13600 (COND ((NULL R) (RETURN E)) ((NULL (CAR R)) (PROOF Z1 Z2) (ERR (QUOTE (QED)))))
13700 (SETQ COUNT (PLUS COUNT (LENGTH R)))
13800 (SETQ R (EDIT U R))
13900 (CLAUSES2 R)
14000 (COND ((NULL R) (RETURN E)))
14100 (BAKSUB CLAUSES R)
14200 (SETQ E (BOOKEEP E R (CONS Z1 Z2)))
14300 (SETQ Z (UNITPN R))
14400 (SETQ UNAXP (APPEND (CAR Z) UNAXP))
14500 (SETQ UNAXN (APPEND (CDR Z) UNAXN))
14600 (SETQ CNT (PLUS CNT (LENGTH R)))
14700 (RETURN E)))
14800 EXPR)
14900
15000 (DEFPROP TRYPRF
15100 (LAMBDA(U)
15200 (PROG (END B1 Z1 Z2 R)
15300 (SETQ END (LAST CLAUSES))
15400 (COND (XX (GO TRY3)))
15500 (SETQ B2 U)
15600 (SETQ E1 (LAST CLAUSES))
15700 TRY1 (SETQ E2 (LAST B2))
15800 (SETQ B1 CLAUSES)
15900 TRY1B
16000 (SETQ XX (CONS B1 B2))
16100 TRY3 (SETQ XX (CHOICE XX E1 B2 E2))
16200 (COND ((NULL XX) (GO TRY7)))
16300 (SETQ Z1 (CAAR XX))
16400 (SETQ Z2 (CADR XX))
16500 (COND ((NOT (HERE Z1)) (RPLACD XX E2) (GO TRY8)) ((NOT (HERE Z2)) (GO TRY8)))
16600 (COND ((NOT STRATEGY) (GO TRY1A)))
16700 (COND ((OR (STRATEGY Z1) (STRATEGY Z2)) (GO TRY1A)) (T (GO TRY8)))
16800 TRY1A
16900 (COND ((AND (ALLPOS Z1) (ALLPOS Z2)) (GO TRY6)) ((AND (ALLNEG Z1) (ALLNEG Z2)) (GO TRY8)))
17000 (SETQ R (RESOLVE Z1 Z2))
17100 (COND ((NULL R) (GO TRY6)) ((MEMQ NIL R) (PROOF Z1 Z2) (RETURN (QUOTE QED))))
17200 (SETQ END (FINI CLAUSES R Z1 Z2 END))
17300 TRY6 (COND (PFLG (GO TRY8)) ((NOT (HERE Z1)) (RPLACD XX E2) (GO TRY8)) ((NOT (HERE Z2)) (GO TRY8)))
17400 (SETQ R (PARMOD Z1 Z2))
17500 (COND ((NULL R) (GO TRY8)))
17600 (SETQ END (FINI CLAUSES R Z1 Z2 END))
17700 TRY8 (COND ((TTYIN) (UPDATE CLAUSES)))
17800 (GO TRY3)
17900 TRY7 (PRINT (QUOTE COUNT))
18000 (PRINT COUNT)
18100 (PRINT (QUOTE LEVEL))
18200 (PRINT LVL)
18300 (SETQ LVL (ADD1 LVL))
18400 (PRINT (QUOTE ELAPSED-TIME))
18500 (PRINT (TIMEIT))
18600 (SETQ E1 (CDR E1))
18700 (COND (ANCESTRY (COND (E1 (SETQ B1 E1) (SETQ E1 END) (GO TRY1B)) (T (GO TRY7A)))))
18800 (SETQ B2 (CDR E2))
18900 (SETQ E1 END)
19000 (COND (E2 (GO TRY1)))
19100 TRY7A
19200 (PRINT (QUOTE NO-PROOF-FOUND))
19300 (COND (AUTO (ERR (QUOTE NOPROOF))))
19400 (UPDATE CLAUSES)
19500 (ERR (QUOTE NOPROOF))
19600 TRY6H))
19700 EXPR)
19800
19900 (DEFPROP UPDATE
20000 (LAMBDA(E)
20100 (PROG (ELOC CHAN AUTO DL1 RF XYZ XYZ1 CMD LOCFLG Z Z1 Z2 INCT Z3 UEX Z1R Z2R N1 R N NAME NAMELIST ZZ)
20200 (SETQ CHAN (OUTC NIL NIL))
20300 (SETQ FNNAM (QUOTE EDI))
20400 (SETQ Z (CONS (QUOTE CLAUSES) E))
20500 (SETQ Z1 (CONS (QUOTE AXIOMS) (AXIOMS1 E)))
20600 (SETQ Z2 (CONS (QUOTE HYPS) (HYPS E)))
20700 (SETQ Z3 (CONS (QUOTE THMS) (THM E)))
20800 (SETQ NAMELIST (CONS Z (CONS Z1 (CONS Z2 (CONS Z3 (CONS (CONS (QUOTE DLIST) DLIST) NEWNAME))))))
20900 (SETQ N1 (LAST NAMELIST))
21000 (SETQ INCT (INC NIL))
21100 U9 (SETQ ELOC E)
21200 (SETQ N 1)
21300 U3 (UP1A (CAR ELOC) N)
21400 U3A (TERPRI)
21500 U3AA (SETQ CMD (READ))
21600 (COND ((EQ CMD (QUOTE ;)) (GO U3AA)))
21700 U3B (COND ((NOT (ATOM CMD)) (GO UPDATE1)))
21800 U3C (SETQ CMD (EXPLODE CMD))
21900 (COND ((EQ (LENGTH CMD) 1) (GO UER1))
22000 ((SETQ Z (ASSOC (READLIST (LIST (CAR CMD) (CADR CMD))) GOLIST)) (GO (CDR Z))))
22100 UER1 (PRINT (QUOTE ILLEGAL-COMMAND))
22200 (GO U3A)
22300 UER2 (PRINT (QUOTE IMPROPER-SYNTAX))
22400 (GO U3A)
22500 UDI1 (SETQ Z1 (UPGETL E NAMELIST))
22600 (COND ((NULL Z1) (GO U3A)))
22700 (CLAUSES Z1)
22800 (GO U3A)
22900 UFL2 (SETQ Z (QUOTE U))
23000 (GO UFL4)
23100 UFL3 (SETQ Z (QUOTE D))
23200 (GO UFL4)
23300 UFL1 (SETQ Z (CAR (EXPLODE (READ))))
23400 UFL4 (SETQ Z2 405104)
23500 (COND ((EQ Z (QUOTE U)) (GO U8)) ((EQ Z (QUOTE D)) (GO U7)) (T (GO UER1)))
23600 UCH1 (SETQ Z (ERRSET (SETQUERY1 (CONS NIL CLAUSES) STRAT)))
23700 (COND (Z (UPDATESTATE (CDAR Z))))
23800 (GO U3A)
23900 UDE1 (SETQ Z2 (UPGETL E NAMELIST))
24000 (COND ((NULL Z2) (GO U3A)))
24100 (EXPUNGE Z2)
24200 (GO U3A)
24300 UIN1 (SETQ NAME (READ))
24400 UIN2 U12
24500 (TERPRI)
24600 (SETQ Z3 (LIST (INCLAUSES)))
24700 UIN2A
24800 (COND ((NULL (CAR Z3)) (PRINT (QUOTE NO-CLAUSES-GIVEN)) (GO U3A))
24900 ((NUMBERP (CAR Z3)) (EVAL (LIST (QUOTE INC) (APPEND (QUOTE (INPUT UPDATE DSK:)) (LIST (READ)))))
25000 (SETQ Z3 (LIST (INCLAUSES)))
25100 (INC NIL)
25200 (GO UIN2A)))
25300 U12B (SETQ Z2 (CAR (SETUP (REVERSE (CAR Z3)))))
25400 (COND ((NULL Z2) (GO U3A)))
25500 UIN3 (SET3 Z2)
25600 UIN3A
25700 (COND ((EQ NAME (QUOTE CLAUSES)) (SETQ END (LAST Z2)) (SETQ Z1 E))
25800 ((SETQ Z1 (ASSOC NAME NAMELIST)) NIL)
25900 (T (GO USE2)))
26000 UIN3B
26100 (COND ((NULL (CAR Z1)) (RPLACD (ASSOC NAME NAMELIST) Z2)) (T (NCONC Z1 Z2)))
26200 (GO U3A)
26300 USU1 (SETQ Z1 (ERRSET (GETTERMS)))
26400 (COND ((NULL Z1) (PRINT (QUOTE HACK-IN-SUBSTITUTION-RETURNING-TO-LISTEN-LOOP)) (GO U3A))
26500 ((NULL (CAR Z1)) (GO U3A)))
26600 (SETQ Z3 NIL)
26700 (SETQ Z1 (CAR Z1))
26800 USU2 (SETQ Z3 (CONS (SUBST1 XYZ XYZ1 (CDAR Z1)) Z3))
26900 (SETQ Z1 (CDR Z1))
27000 (COND (Z1 (GO USU2)) (T (SETQ Z3 (LIST Z3)) (SETQ NAME (QUOTE ASSERT)) (GO U12B)))
27100 UUP1 (SETQ Z2 (UPGETNU))
27200 (COND ((NUMBERP Z2) (GO U8)) (T (GO U3A)))
27300 UDO1 (SETQ Z2 (UPGETNU))
27400 (COND ((NUMBERP Z2) (GO U7)) (T (GO U3A)))
27500 UAN1 (SETQ Z2 (UPGETL E NAMELIST))
27600 UAN2 (COND (Z2 (PROOF1 (CAR Z2))) (T (GO U3A)))
27700 (SETQ Z2 (CDR Z2))
27800 (GO UAN2)
27900 UTE1 (COND ((EQ (CAR (LAST CMD)) (QUOTE ;)) (SETQ Z NIL)) (T (SETQ Z (UPGETL E NAMELIST))))
28000 (INC INCT)
28100 (OUTC CHAN NIL)
28200 (SETQ DLIST (GETNAME (QUOTE DLIST) NAMELIST))
28300 (SETQ Z1
28400 (APPEND (GETNAME (QUOTE AXIOMS) NAMELIST)
28500 (GETNAME (QUOTE HYPS) NAMELIST)
28600 (GETNAME (QUOTE THMS) NAMELIST)))
28700 (RETURN (MINIMIZE (APPEND Z1 Z)))
28800 USA1 (SETQ Z2 (UPGETL E NAMELIST))
28900 (COND (Z2 (SETQ NAME (QUOTE CLAUSES)) (GO UIN3A)) (T (GO U3A)))
29000 UPA1 (SETQ Z1 (UPGETL E NAMELIST))
29100 (SETQ Z2 (UPGETL E NAMELIST))
29200 (COND ((AND Z1 Z2) (SETQ RF NIL) (GO URE1A)) (T (GO U3A)))
29300 USI1 (COND ((NULL (SETQ Z1 (UPGETL E NAMELIST))) (GO U3A)))
29400 (COND ((NOT (EQ (READ) (QUOTE BY))) (GO UER2)))
29500 (COND ((NULL (SETQ Z2 (UPGETL E NAMELIST))) (GO U3A)))
29600 (SETQ Z3 Z1)
29700 USI2 (DEMOD (LIST (CAR Z3)) Z2)
29800 (SETQ Z3 (CDR Z3))
29900 (COND (Z3 (GO USI2)))
30000 (PRINT (QUOTE CLAUSES-ARE:))
30100 (CLAUSES Z1)
30200 (GO U3A)
30300 UAS1 (SETQ NAME (QUOTE ASSUMPTIONS))
30400 (SETQ LOCFLG T)
30500 UAS1A
30600 (COND ((SETQ Z1 (ASSOC NAME NAMELIST)) (RPLACA Z1 (QUOTE %%))))
30700 (GO UIN2)
30800 UCU1 (QUERY)
30900 (GO U3A)
31000 UDS1 (SETQ Z1 (READ))
31100 (COND ((NOT (ATOM Z1)) (GO UDS3)))
31200 UDS2 (COND
31300 ((EQ (CAR (SETQ Z2 (REVERSE (EXPLODE Z1)))) (QUOTE ;)) (SETQ Z1 (READLIST (REVERSE (CDR Z2))))
31400 (GO UDS2)))
31500 UDS3 (SETQ CHAN1 (EVAL (LIST (QUOTE OUTC) (LIST (QUOTE OUTPUT) (QUOTE EDIT) (QUOTE DSK:) Z1) NIL)))
31600 (GO U3A)
31700 UEO1 (OUTC CHAN1 T)
31800 (GO U3A)
31900 UUS1 (SETQ NAME (QUOTE USING))
32000 (SETQ LOCFLG T)
32100 UUS2 (SETQ Z2 (UPGETL E NAMELIST))
32200 (COND ((NULL Z2) (GO U3A)))
32300 USE2 (COND ((SETQ Z1 (ASSOC NAME NAMELIST)) (RPLACD Z1 Z2)))
32400 (COND (LOCFLG (SETQ LOCFLG NIL) (RPLACD NAMELIST (CONS (CONS NAME Z2) (CDR NAMELIST))))
32500 (T (RPLACA (CAR N1) NAME)
32600 (RPLACD (CAR N1) Z2)
32700 (RPLACD N1 (CONS (CONS NIL NIL) NIL))
32800 (SETQ N1 (CDR N1))))
32900 (GO U3A)
33000 USE1 (SETQ NAME (READ))
33100 (GO UUS2)
33200 UCL1 (SETQ Z (READ))
33300 UCL2 (COND ((SETQ Z1 (ASSOC Z NAMELIST)) (RPLACA Z1 (QUOTE %%)) (GO U3A))
33400 ((EQ (CAR (SETQ Z (REVERSE (EXPLODE Z)))) (QUOTE ;)) (SETQ Z (READLIST (REVERSE (CDR Z))))
33500 (GO UCL2))
33600 (T (GO U3A)))
33700 UGO1 (SETQ Z1 (UPGETNU))
33800 (COND ((NOT (NUMBERP Z1)) (GO U3A)))
33900 (COND ((SETQ Z (DOWN Z1 E)) (SETQ ELOC Z) (SETQ N Z1) (GO U3))
34000 (T (PRINT (QUOTE NO-SUCH-CLAUSE)) (GO U3A)))
34100 UTR1 (SETQ UEX NIL)
34200 (GO UEX2)
34300 UEX1 (SETQ UEX T)
34400 UEX2 (SETQ NAME (QUOTE LEMMA))
34500 (SETQ Z1
34600 (INITIALAX
34700 (APPEND (GETNAME (QUOTE NEGLEMMA) NAMELIST)
34800 (CONS NIL (GETNAME (QUOTE ASSUMPTIONS) NAMELIST))
34900 (CONS NIL (GETNAME (QUOTE USING) NAMELIST)))))
35000 (COND ((NULL (CAR Z1)) (PRINT (QUOTE NOTHING-TO-PROVE)) (GO U3A)))
35100 (SETQ Z2
35200 (ATTEMPT (CONS Z1 (FIXSET Z1))
35300 (COND (UEX (RESET1 STRATEGY (SUPPORT (LIST (CAR Z1))))) (T NIL))
35400 NIL))
35500 (GO AT1A)
35600 UST1 (STOP)
35700 (GO U3A)
35800 UAB1 (COND ((EQ (CAR (LAST CMD)) (QUOTE ;)) (SETQ Z1 NIL)) (T (SETQ Z1 (UPGETL E NAMELIST))))
35900 (ERR Z1)
36000 U8 (COND ((EQ Z2 0) (GO U9)))
36100 U83 (COND ((NULL Z2) (GO U3A)) ((TTYIN) (GO U3A)) ((LESSP Z2 5) (SETQ ZZ Z2) (SETQ Z2 NIL) (GO U84)))
36200 (SETQ Z2 (DIFFERENCE Z2 5))
36300 (SETQ ZZ 5)
36400 U84 (SETQ Z N)
36500 (SETQ Z3 (DIFFERENCE N ZZ))
36600 (COND ((OR (ZEROP Z3) (MINUSP Z3)) (SETQ Z3 1) (SETQ Z2 NIL)))
36700 (SETQ N Z3)
36800 (SETQ Z3 ELOC)
36900 (SETQ ELOC (DOWN N E))
37000 (SETQ ZZ NIL)
37100 (SETQ Z1 ELOC)
37200 U81 (COND ((EQ Z1 Z3) (GO U82)))
37300 (SETQ ZZ (CONS (CAR Z1) ZZ))
37400 (SETQ Z1 (CDR Z1))
37500 (GO U81)
37600 U82 (COND ((NULL ZZ) (GO U83)))
37700 (UP1A (CAR ZZ) (SUB1 Z))
37800 (SETQ ZZ (CDR ZZ))
37900 (SETQ Z (SUB1 Z))
38000 (GO U82)
38100 U7 (COND ((ZEROP Z2) (SETQ ELOC (LAST ELOC)) (SETQ N (LENGTH E)) (GO U3)))
38200 (SETQ Z2 (PLUS Z2 N))
38300 U7A (COND ((NULL (CDR ELOC)) (PRINT (QUOTE END)) (GO U3A)))
38400 (SETQ ELOC (CDR ELOC))
38500 (SETQ N (ADD1 N))
38600 (UP1A (CAR ELOC) N)
38700 (COND ((EQ N Z2) (GO U3A)) ((TTYIN) (GO U3A)) (T (GO U7A)))
38800 UPR1 (TERPRI)
38900 (SETQ Z3 (JUSTCLAUSE))
39000 UPR1A
39100 (COND ((NULL Z3) (PRINT (QUOTE NO-CLAUSES-GIVEN)) (GO U3A))
39200 ((NUMBERP Z3) (EVAL (LIST (QUOTE INC) (APPEND (QUOTE (INPUT UPDATE DSK:)) (LIST (READ)))))
39300 (SETQ Z3 (JUSTCLAUSE))
39400 (INC NIL)
39500 (GO UPR1A)))
39600 (SETQ Z2 (CNF (COPY Z3)))
39700 (SETQ Z3 (CNF (LIST (QUOTE NOT) (FIXQFF Z3))))
39800 (SETQ Z2 (SET3 (CAR (SETUP Z2))))
39900 (SETQ Z3 (SET3 (CAR (SETUP Z3))))
40000 (SETQ Z1 (ASSOC (QUOTE NEGLEMMA) NAMELIST))
40100 (COND (Z1 (RPLACD Z1 Z3)) (T (RPLACD NAMELIST (CONS (CONS (QUOTE NEGLEMMA) Z3) (CDR NAMELIST)))))
40200 (SETQ NAME (QUOTE LEMMA))
40300 (SETQ LOCFLG T)
40400 (GO USE2)
40500 UME1 (SETQ Z1 (UPGETL E NAMELIST))
40600 (SETQ Z2 (UPGETL E NAMELIST))
40700 (COND ((OR (NULL Z1) (NULL Z2)) (GO U3A)))
40800 (BAKSUB Z1 Z2)
40900 (GO U3A)
41000 UHE1 (PRINT
41100 (QUOTE
41200 "
41300 THE FOLLOWING COMMANDS ARE AVAILABLE TO THE CLAUSES EDITOR:
41400
41500 DELETE, #,# ...# .....DELETE THE SPECIFIED CLAUSES
41600 RESOLVE #,# ..........RESOLVE THE PAIR AND ASSIGN THE RESULT TO RESOLVE
41700 PARAMODULATE(AAAG--SEE NOTE!!) #,#
41800 ANCESTRY,# ...........PRINT THE PROOF TREE OF CLAUSE #.
41900 FLOAT,UP .............MOVE THE POINTER UP, PRINTING AS WE GO
42000 FLOAT,DOWN ...........GUESS WHAT
42100 UP,# ................MOVE UP # CLAUSES, PRINTING AS WE GO
42200 DOWN,#
42300 CLEAR,NAME ...........NAME IS A COLLECTION OF CLAUSES,RESET NAME
42400 INSERT, NAME ........THE CLAUSES THEN TYPED ARE ASSIGNED TO NAME
42500 IF NAME IS UNASSIGNED A NEW COLLECTION IS MADE
42600
42700 SAVE ,NAME.............THE SPECIFIED CLAUSES ARE APPENDED TO THE CLAUSE LIST
42800 MERGE,NAME1,NAME2......DELETE THE ELEMENTS OF NAME1 SUBSUMED BY ELEMENTS OF NAME2.
42900 SET NAME #,# ...# .....ASSIGNS THE SELECTED CLAUSES TO NAME
43000 EDIT TYPE 'TE'.
43100 GO,# . .......... MOVE THE POINTER TO CLAUSE #.
43200 EXECUTE
43300 ABORT
43400 TERMINATE ............TERMINATE THE EDIT
43500 STOP ..............STOP HALTS THE PROVER . TO CONTINUE TYPE 'ST '.
43600 ASSUME,C[1];C[2]; ...C[N];;
43700 USING,NAME,(NAME #,#...#), ETC.
43800 PROVE,C;;
43900 SUBS T1 FOR T2 IN (NAME #)..GENERATES A NEW CLAUSE WITH
44000 T1 SUBSTITUTED FOR T2 IN CLAUSE (NAME #)
44100 THE CLAUSE IS ADDED TO THE NAME 'ASSERT'.
44200 EVAL
44300 DISPLAY,NAME .......PRINTS THE CLAUSES ASSOCIATED WITH NAME
44400 HELP ..............HELP TYPES THIS LIST
44500
44600 IT IS SUFFICIENT TO SPECIFY THE FIRST TWO CHARACTERS OF
44700 A COMMAND. E.G.,FL,UP FOR FLOAT,UP. FU AND FD WILL ALSO
44800 SUFFICE FOR FLOAT,UP AND FLOAT,DOWN.
44900 ")) (GO U3A)
45000 URE1 (SETQ Z1 (UPGETL E NAMELIST))
45100 (SETQ Z2 (UPGETL E NAMELIST))
45200 U%RE1
45300 (SETQ RF T)
45400 URE1A
45500 (COND ((OR (NULL Z1) (NULL Z2)) (GO U3A)))
45600 (SETQ Z1R Z1)
45700 (SETQ Z2R Z2)
45800 (SETQ Z3 (LIST NIL))
45900 (SETQ ZZ Z3)
46000 (COND ((OR (NULL Z1) (NULL Z2)) (GO UR3B)))
46100 (COND ((NOT RF) (SETQ DL1 DLIST) (SETQ DLIST NIL)))
46200 UR3 (COND ((AND RF (ALLPOS (CAR Z1R)) (ALLPOS (CAR Z2R))) (GO UR3A))
46300 ((AND (ALLNEG (CAR Z1R)) (ALLNEG (CAR Z2R))) (GO UR3A)))
46400 (COND (RF (SETQ R (RESOLVE (CAR Z1R) (CAR Z2R)))) (T (SETQ R (PARMOD (CAR Z1R) (CAR Z2R)))))
46500 (COND ((NULL R) (GO UR3A)) ((MEMQ NIL R) (PROOF (CAR Z1R) (CAR Z2R)) (GO U3A)))
46600 (SETQ Z3 (BOOKEEP Z3 R (CONS (CAR Z1R) (CAR Z2R))))
46700 UR3A (SETQ Z2R (CDR Z2R))
46800 (COND (Z2R (GO UR3)))
46900 (SETQ Z1R (CDR Z1R))
47000 (COND (Z1R (SETQ Z2R Z2) (GO UR3)))
47100 UR3B (SETQ Z3 (CDR ZZ))
47200 (COND ((NULL Z3)
47300 (COND (RF (PRINT (QUOTE NO-RESOLVENTS)) (GO U3A))
47400 (T (PRINT (QUOTE NO-PARMODULANTS)) (SETQ DLIST DL1) (GO U3A))))
47500 (RF (SETQ NAME (QUOTE RES)))
47600 (T (SETQ NAME (QUOTE PAR)) (SETQ DLIST DL1)))
47700 (SETQ Z2 Z3)
47800 (SETQ LOCFLG T)
47900 (GO AT2A)
48000 UEV1 (PRINT (QUOTE EVAL-AWAITS))
48100 (SETQ Z2 (ERRSET (EVAL (READ))))
48200 (COND (Z2 (PRINT (CAR Z2)) (GO UE2)) (T (PRINT (QUOTE LOSE)) (GO UEV1)))
48300 UE2 (COND ((EQ (QUOTE END) (CAR Z2)) (GO U3A)))
48400 (GO UEV1)
48500 UPDATE1
48600 (SETQ Z (EXPLODE (CAR CMD)))
48700 (COND ((SETQ Z (ASSOC (READLIST (LIST (CAR Z) (CADR Z))) GOLIST1)) (GO (CDR Z))) (T (GO UER1)))
48800 AT1 (COND ((NULL (SETQ Z1 (GETNAME (CADR CMD) NAMELIST))) (GO U3A)))
48900 (SETQ NAME (CADR CMD))
49000 (SETQ XYZ Z1)
49100 (RPLACA (CDR CMD) (QUOTE XYZ))
49200 (RPLACA CMD (QUOTE ATTEMPTUNTIL))
49300 (SETQ Z2 (EVAL CMD))
49400 AT1A (UPDATESTATE STRAT)
49500 (COND ((OR (NULL Z2) (EQ (CAR Z2) (QUOTE NOPROOF))) (PRINT (QUOTE ATTEMPT-ABORTED-FOR:))
49600 (PRINC NAME)
49700 (GO U3A))
49800 ((EQ (CAR Z2) (QUOTE QED)) (PRINT (QUOTE CONTRADICTION-FOUND-FOR:)) (PRINC NAME) (GO U3A)))
49900 AT2A (SETQ N 1)
50000 AT2 (COND ((ASSOC (READLIST (APPEND (EXPLODE NAME) (EXPLODE N))) NAMELIST) (SETQ N (ADD1 N)) (GO AT2)))
50100 (SETQ NAME (READLIST (APPEND (EXPLODE NAME) (EXPLODE N))))
50200 (PRINT (QUOTE THE-PROVER-RETURNS-THE-FOLLOWING-LOVELY-CLAUSES:))
50300 (PRINT (QUOTE THEY-WILL-BE-FOUND-UNDER-THE-NAME:))
50400 (PRIN1 NAME)
50500 (CLAUSES Z2)
50600 (GO USE2)
50700 S1 (COND ((NULL (SETQ XYZ (GETNAME (CADDDR CMD) NAMELIST))) (GO U3A)))
50800 (RPLACA (CDDDR CMD) (QUOTE XYZ))
50900 (RPLACA CMD (QUOTE SAVE))
51000 (EVAL CMD)
51100 (GO U3A)))
51200 EXPR)